@$i$: with declarations ds:${\it ds}$da:${\it da}$ $k$(v) sends $f$ s v on link $l$($j$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if eqof(IdDeq)($j$,$i$)$\rightarrow$ with declarations ds:${\it ds}$da:${\it da}$$k$(v) sends $f$ s v on link $l$ else  fi